Nuprl Lemma : possible-event_wf
0,22
postcript
pdf
poss
:(ES{i}
Prop{i'}). possible-event{i:l}(
poss
)
Prop{i'}
latex
Definitions
Type
,
Prop
,
t
T
,
ES
,
x
:
A
B
(
x
)
,
f
(
a
)
,
x
:
A
.
B
(
x
)
,
E
,
x
:
A
B
(
x
)
,
PossibleEvent(
poss
)
Lemmas
es-E
wf
,
event
system
wf
origin
poss:(ES{i}
Prop{i'}). possible-event{i:l}(poss) 
Prop{i'} poss:(ES{i}Prop{i'}). possible-event{i:l}(poss) Prop{i'} TB(x)x:A. B(x)
B(x)